Nuprl Lemma : CV_property
11,40
postcript
pdf
F
,
t
:Top. (CV(
F
)(
t
)) ~ (
F
(
t
,CV(
F
)))
latex
Definitions
x
:
A
.
B
(
x
)
,
CV(
F
)
,
Y
,
t
T
Lemmas
top
wf
origin
F, t:Top. (CV(F)(t)) ~ (F(t,CV(F))) F, t:Top. (CV(F)(t)) ~ (F(t,CV(F))) x:A. B(x)
T